Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    x - 0  → x
2:    s(x) - s(y)  → x - y
3:    0 + y  → y
4:    s(x) + y  → s(x + y)
5:    x * 0  → 0
6:    x * s(y)  → x + (x * y)
7:    f(s(x))  → f((s(s(0)) * s(x)) - s(s(x)))
There are 7 dependency pairs:
8:    s(x) -# s(y)  → x -# y
9:    s(x) +# y  → x +# y
10:    x *# s(y)  → x +# (x * y)
11:    x *# s(y)  → x *# y
12:    F(s(x))  → F((s(s(0)) * s(x)) - s(s(x)))
13:    F(s(x))  → (s(s(0)) * s(x)) -# s(s(x))
14:    F(s(x))  → s(s(0)) *# s(x)
The approximated dependency graph contains 4 SCCs: {9}, {11}, {8} and {12}.
Tyrolean Termination Tool  (0.03 seconds)   ---  May 3, 2006